basic
Inverse(T;op;id;inv) == x:T. (x op (inv(x))) = id & ((inv(x)) op x) = id 

latex

---

clarification:

basic
Inverse(T;op;id;inv) == x:T. (x op (inv(x))) = id  T & ((inv(x)) op x) = id  T 

latex

Up	gen algebra 1
Wellformedness Lemmas	inverse wf
Definitions	x:A. B(x), P & Q, x f y